app2(app2(ack, 0), y) -> app2(succ, y)
app2(app2(ack, app2(succ, x)), y) -> app2(app2(ack, x), app2(succ, 0))
app2(app2(ack, app2(succ, x)), app2(succ, y)) -> app2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
↳ QTRS
↳ DependencyPairsProof
app2(app2(ack, 0), y) -> app2(succ, y)
app2(app2(ack, app2(succ, x)), y) -> app2(app2(ack, x), app2(succ, 0))
app2(app2(ack, app2(succ, x)), app2(succ, y)) -> app2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
APP2(app2(ack, app2(succ, x)), y) -> APP2(ack, x)
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(app2(ack, app2(succ, x)), y)
APP2(app2(ack, app2(succ, x)), y) -> APP2(succ, 0)
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(ack, x)
APP2(app2(ack, app2(succ, x)), y) -> APP2(app2(ack, x), app2(succ, 0))
APP2(app2(ack, 0), y) -> APP2(succ, y)
app2(app2(ack, 0), y) -> app2(succ, y)
app2(app2(ack, app2(succ, x)), y) -> app2(app2(ack, x), app2(succ, 0))
app2(app2(ack, app2(succ, x)), app2(succ, y)) -> app2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
APP2(app2(ack, app2(succ, x)), y) -> APP2(ack, x)
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(app2(ack, app2(succ, x)), y)
APP2(app2(ack, app2(succ, x)), y) -> APP2(succ, 0)
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(ack, x)
APP2(app2(ack, app2(succ, x)), y) -> APP2(app2(ack, x), app2(succ, 0))
APP2(app2(ack, 0), y) -> APP2(succ, y)
app2(app2(ack, 0), y) -> app2(succ, y)
app2(app2(ack, app2(succ, x)), y) -> app2(app2(ack, x), app2(succ, 0))
app2(app2(ack, app2(succ, x)), app2(succ, y)) -> app2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(app2(ack, app2(succ, x)), y)
APP2(app2(ack, app2(succ, x)), y) -> APP2(app2(ack, x), app2(succ, 0))
app2(app2(ack, 0), y) -> app2(succ, y)
app2(app2(ack, app2(succ, x)), y) -> app2(app2(ack, x), app2(succ, 0))
app2(app2(ack, app2(succ, x)), app2(succ, y)) -> app2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
APP2(app2(ack, app2(succ, x)), y) -> APP2(app2(ack, x), app2(succ, 0))
Used ordering: Combined order from the following AFS and order.
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(app2(ack, app2(succ, x)), y)
app2 > ack > 0 > succ
app2(app2(ack, app2(succ, x)), app2(succ, y)) -> app2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
app2(app2(ack, app2(succ, x)), y) -> app2(app2(ack, x), app2(succ, 0))
app2(app2(ack, 0), y) -> app2(succ, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(app2(ack, app2(succ, x)), y)
app2(app2(ack, 0), y) -> app2(succ, y)
app2(app2(ack, app2(succ, x)), y) -> app2(app2(ack, x), app2(succ, 0))
app2(app2(ack, app2(succ, x)), app2(succ, y)) -> app2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(app2(ack, app2(succ, x)), app2(succ, y)) -> APP2(app2(ack, app2(succ, x)), y)
succ > app1 > APP1
succ > ack
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
app2(app2(ack, 0), y) -> app2(succ, y)
app2(app2(ack, app2(succ, x)), y) -> app2(app2(ack, x), app2(succ, 0))
app2(app2(ack, app2(succ, x)), app2(succ, y)) -> app2(app2(ack, x), app2(app2(ack, app2(succ, x)), y))